FDL - Step of Proof: comp_nat_ind_tp

Step of Proof: comp_nat_ind_tp

Inference at * 1 1 1 1
Iof proof for Lemma comp nat ind tp:

.....assertion..... NILNIL

1. P :

{k}
2.

i:

. (

j:

. (j < i)

P(j))

P(i)
3.

zz,i:

. (i < zz)

P(i)

by (\p.Thin (get_int_arg `hn` p) p)

1:

1: 2.

i:

. (

j:

. (j < i)

P(j))

P(i)

1:

zz,i:

. (i < zz)

P(i)

.